package bcontractor.propositional.factories;

import static bcontractor.propositional.MiniSatReasonerBuilder.aMiniSatReasoner;
import static org.hamcrest.CoreMatchers.is;
import static org.junit.Assert.assertThat;

import java.util.Random;

import org.junit.Before;
import org.junit.Test;

import bcontractor.api.SATReasoner;
import bcontractor.api.SentenceSet;
import bcontractor.propositional.PropositionalSentence;

/**
 * Tests a contraction case factory build using propositional factories
 * @author lundberg
 * 
 */
public class ContractionCaseFactoryShould {

	private static final int samples = 100;

	private static final int minSize = 5;

	private static final int maxSize = 8;

	private static final int nVariables = 10;

	private static final int nClauses = 50;

	private ContractionCaseFactory<PropositionalSentence> factory;

	private SATReasoner<PropositionalSentence> reasoner;

	@Before
	public void initialize() {
		Random random = new Random(31L);
		ArbitraryClauseFactory sentenceFactory = new ArbitraryClauseFactory(random, nVariables, minSize, maxSize);
		PropositionalSentenceSetFactory sentenceSetFactory = new PropositionalSentenceSetFactory(sentenceFactory, nVariables, nClauses);
		reasoner = aMiniSatReasoner().build();
		factory = new ContractionCaseFactory<PropositionalSentence>(sentenceSetFactory, sentenceFactory, reasoner);
	}

	@Test
	public void shouldGenerateReasonableCases() {
		for (int i = 0; i < samples; i++) {
			ContractionCase<PropositionalSentence> contractionCase = factory.create();
			SentenceSet<PropositionalSentence> sentences = contractionCase.getSentences();
			PropositionalSentence sentence = contractionCase.getSentence();
			assertThat(reasoner.isSatisfiable(sentences), is(true));
			assertThat(reasoner.entails(sentences, sentence), is(true));
			assertThat(reasoner.isUnsatisfiable(sentences.with(sentence.negate())), is(true));
		}
	}
}
